Nuprl Lemma : q-constraints_wf
11,40
postcript
pdf
A
:((
:(
)
) List),
k
:
,
y
:(
List). q-constraints(
k
;
A
;
y
)
latex
Definitions
False
,
A
,
P
Q
,
x
.
t
(
x
)
,
A
B
,
A
c
B
,
q-constraints(
k
;
A
;
y
)
,
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
Lemmas
l
member
wf
,
pi1
wf
,
q-linear
wf
,
pi2
wf
,
q-rel
wf
,
nat
wf
,
l
all
wf2
,
rationals
wf
,
length
wf1
origin
A:((:(
) 
) List), k:, y:( List). q-constraints(k;A;y) 
A:((:() ) List), k:, y:( List). q-constraints(k;A;y) 
A
Q
x. t(x)
B
B Tx:A. B(x)